#include "sat.hpp"
#include "parser.hpp"

////////////////////////////////////////////////////////////////////////////////
//               ICI LES FONCTIONS SONT A IMPLEMENTER                         //
////////////////////////////////////////////////////////////////////////////////

lit_t tseitin(formule f, const map<string, unsigned int> & m, cnf_t & c, var_t & next)
{

	switch(f->op)
	{
	case o_variable :
	{
		return var2lit(m.at(*f->nom));
	}

	case o_non :
	{
		return neg(tseitin(f->arg, m, c, next));
	}

	break;

	case o_ou :
	{
		lit_t var1 = tseitin(f->arg1, m, c, next);
		lit_t var2 = tseitin(f->arg2, m, c, next);
		lit_t var = var2lit(next);
		next++;

		cls_t cl;

		//(¬p ∨ p1 ∨ p2)
		cl.insert(neg(var));
		cl.insert(var1);
		cl.insert(var2);

		c.push_back(cl);

		cl.clear();
		// (p ∨ ¬p1)
		cl.insert(var);
		cl.insert(neg(var1));
		// (p ∨ ¬p2)
		c.push_back(cl);
		cl.clear();

		cl.insert(var);
		cl.insert(neg(var2));

		c.push_back(cl);
		cl.clear();

		return var;
	}
	break;

	case o_et :
	{
		lit_t var1 = tseitin(f->arg1, m, c, next);
		lit_t var2 = tseitin(f->arg2, m, c, next);
		lit_t var = var2lit(next);
		next++;

		cls_t cl;

		// (p ∨ ¬p1 ∨ ¬p2) ∧ (¬p ∨ p1) ∧ (¬p ∨ p2)
		cl.insert(var);
		cl.insert(neg(var1));
		cl.insert(neg(var2));

		c.push_back(cl);
		cl.clear();

		cl.insert(neg(var));
		cl.insert(var1);

		c.push_back(cl);
		cl.clear();

		cl.insert(neg(var));
		cl.insert(var2);

		c.push_back(cl);
		cl.clear();

		return var;
	}
	break;
	case o_implique :
	{
		lit_t var1 = tseitin(f->arg1, m, c, next);
		lit_t var2 = tseitin(f->arg2, m, c, next);
		lit_t var = var2lit(next);
		next++;

		cls_t cl;

		//(¬p ∨ ¬p1 ∨ p2) ∧ (p ∨ p1) ∧ (p ∨ ¬p2)
		cl.insert(neg(var));
		cl.insert(neg(var1));
		cl.insert(var2);

		c.push_back(cl);
		cl.clear();

		cl.insert(var);
		cl.insert(var1);

		c.push_back(cl);
		cl.clear();

		cl.insert(var);
		cl.insert(neg(var2));

		c.push_back(cl);
		cl.clear();

		return var;
	}
	break;

	case o_equivaut :
	{
		lit_t var1 = tseitin(f->arg1, m, c, next);
		lit_t var2 = tseitin(f->arg2, m, c, next);
		lit_t var = var2lit(next);

		next++;

		cls_t cl;

		// (¬p ∨ ¬p1 ∨ p2) ∧ (¬p ∨ p1 ∨ ¬p2) ∧ (p ∨ p1 ∨ p2) ∧ (p ∨ ¬p1 ∨ ¬p2)
		cl.insert(neg(var));
		cl.insert(neg(var1));
		cl.insert(var2);

		c.push_back(cl);
		cl.clear();

		cl.insert(neg(var));
		cl.insert(var1);
		cl.insert(neg(var2));

		c.push_back(cl);
		cl.clear();

		cl.insert(var);
		cl.insert(var1);
		cl.insert(var2);

		c.push_back(cl);
		cl.clear();

		cl.insert(var);
		cl.insert(neg(var1));
		cl.insert(neg(var2));

		c.push_back(cl);
		cl.clear();

		return var;
	}
	break;
	}

	return 0;
}

cnf_t tseitin(formule f)
{
	map<string, unsigned int> m;

	numerote(f, m);

	cnf_t c;

	var_t sizeMap = m.size();

	tseitin(f, m, c, sizeMap);

	return c;

	//ECRIRE TEST (VOIR SITE WEB LIF11)
}


val_t valeur_lit(const vector<val_t> & valeurs, lit_t l)
{
	val_t retour = valeurs[l];
	if(retour == INDETERMINEE)
	{
		return retour;
	}
	if(positif(l))
	{
		if(retour == VRAI)
		{
			return FAUX;
		}
		else
		{
			return retour;
		}
	}
	return retour;
}

val_t valeur_clause(const vector<val_t> & valeurs, cls_t clause)
{
	bool indet = false;

	for ( cls_t::const_iterator it = clause.begin(); it != clause.end(); it++ )
	{
		if(valeur_lit(valeurs, *it) == VRAI)
		{
			return VRAI;
		}
		if(valeur_lit(valeurs, *it) == INDETERMINEE)
		{
			indet = true;
		}
	}

	if(indet == true)
	{
		return INDETERMINEE;
	}

	return FAUX;
}

val_t valeur_cnf(const vector<val_t> & valeurs, cnf_t cnf)
{
	bool indet = false;

	for (unsigned int i = 0; i < cnf.size(); i++)
	{
		if(valeur_clause(valeurs, cnf[i]) == FAUX)
		{
			return FAUX;
		}
		if(valeur_clause(valeurs, cnf[i]) == INDETERMINEE)
		{
			indet = true;
		}
	}

	if(indet == true)
	{
		return INDETERMINEE;
	}

	return VRAI;
}

bool cherche(vector<val_t> & valeurs, var_t suiv, const cnf_t & cnf)
{
	valeurs[suiv] = VRAI;

	if(suiv == valeurs.size() - 1)
	{
		cherche(valeurs, suiv + 1, cnf);
	}
	else
	{
		if(valeur_cnf(valeurs, cnf) == VRAI)
		{
			return true;
		}
		else
		{
			valeurs[suiv] = FAUX;
			if(valeur_cnf(valeurs, cnf) == VRAI)
			{
				return true;
			}
			else
			{
				valeurs[suiv] = INDETERMINEE;
				return false;
			}
		}
	}


	return false;
}

formule applique(formule f, const map<string,formule> & substitution)
{
	//TEST
	//Faire une formule
	//Faire une substitution à la main
	//2ème formule qui correspond à la formule substitué
	//Appeler applique() sur la première formule
	//F1 == F2 ?
	switch(f->op)
	{
	case o_variable:
		return substitution.find(*f->nom)->second;
		break;

	case o_non:
		return non(applique(f->arg, substitution));
		break;

	case o_et:
		return et(applique(f->arg1, substitution), applique(f->arg2, substitution));
		break;

	case o_ou:
		return ou(applique(f->arg1, substitution), applique(f->arg2, substitution));
		break;

	case o_implique:
		return impl(applique(f->arg1, substitution), applique(f->arg2, substitution));
		break;

	case o_equivaut:
		return equiv(applique(f->arg1, substitution), applique(f->arg2, substitution));
		break;
	}
	return NULL;
}

vector<formule> additionneur(int taille)
{

	vector<formule> v;
	formule somme = lit_formule("t <=> ( u <=> w )");
	formule retenue = lit_formule("( t => ( u \\/ w )) /\\ ( ~t => ( u /\\ w ))");
	formule A1,B;

	map<string,formule> substitution;

	substitution.insert(pair<string,formule>("p1", lit_formule("t")));
	substitution.insert(pair<string,formule>("q1", lit_formule("u")));
	substitution.insert(pair<string,formule>("0", lit_formule("w")));

	if(taille == 1)
	{
		A1 = applique(somme, substitution);
		B = applique(retenue, substitution);

		v.push_back(B);
		v.push_back(A1);

		return v;
	}
	else 
	{

	}

	return v;
				}

vector<vector<cls_t>> indexe_clauses(const cnf_t& cnf)
				{
	vector<vector<cls_t> > v;
	int meilleurL;

	for(unsigned int i = 0 ; i < cnf.size() ; i++)
	{
		for (set<lit_t>::iterator it = cnf[i].begin() ; it != cnf[i].end(); it++)
		{
			if(meilleurL < *it)
			{
				meilleurL = *it;
			}
		}
	}

	v.resize(meilleurL + 1);

	for(unsigned int i = 0 ; i < v.size() ; i++)
	{
		for(unsigned int j = 0 ; j < cnf.size() ; j++)
		{
			if(cnf[j].count(i) > 0)
			{
				v[i].push_back(cnf[j]);
			}
		}
	}



	return v;
				}

bool contient_insatisfaite(var_t variable,
		const vector<val_t>& valeurs,
		const vector<vector<cls_t> >& index_clauses)
{
	vector<unsigned int> valeursTemp;
	lit_t l = var2lit(variable);
    
    //on parcourt la/les clause(s) dans laquelle/lesquelles se trouve l
    for(unsigned int i = 0; i < index_clauses[l].size() ; i++)
	{
        cout << index_clauses[l][i] << endl;

        //on parcourt les littéraux de la clause
        
        for(set<lit_t>::iterator it = index_clauses[l][i].begin(); it != index_clauses[l][i].end(); ++it)
		{
			valeursTemp.push_back(valeurs[*it]);
        }

		unsigned int nbLitterauxFaux = 0;
        for(unsigned int j = 0 ; j < valeursTemp.size() ; j++)
        {
            //si la valeur est vrai, clause satisfialbe, on renvoie false.
            //ICI, test positif(valeursTemp[j]) PAS SUR POUR CA
            /*if(negatif){
            if(valeursTemp[j] == VRAI)
            {
                return false;
            }
            }
            else
            {
                if(valeursTemp[j] == FAUX){
                    nbLitterauxFaux++;
                }
            }*/
        }
        if(nbLitterauxFaux == valeursTemp.size())
        {
            return true;
        }
    }
	return true;
}

vector<var_t> propage(lit_t lit, vector<val_t> & valeurs, cnf_t & cnf, vector<vector<cls_t> > & index)
				{
	vector<var_t> v;
	lit_t temp;

	vector<lit_t> listeCourante;
	listeCourante.push_back(lit);

	while(listeCourante.size() > 0)
	{
		temp = listeCourante[0];
		//listeCourante.erase(temp);

		if(valeurs[temp] == NULL)
		{
			valeurs[temp] = INDETERMINEE;
		}


	}

	return v;
				}
